(*
 * Copyright (c) 2009, Palle Raabjerg
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 *   * Redistributions of source code must retain the above copyright notice,
 *     this list of conditions and the following disclaimer.
 *   * Redistributions in binary form must reproduce the above copyright notice,
 *     this list of conditions and the following disclaimer in the documentation
 *     and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE
 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
 * POSSIBILITY OF SUCH DAMAGE.
 *)

module SMap = Map.Make(String);;
module SSet = Set.Make(String);;

type term = Const of string
	    | Var of string
	    | FuncApp of string*(term list);;
type pre = PPredicate of string*(term list)
	   | NegPredicate of string*(term list)
	   | PreAnd of pre*pre
	   | Or of pre*pre
	   | Exists of string*pre
	   | Equal of term*term
	   | NEqual of term*term;;
type cl = CPredicate of string*(term list)
	  | Truth
	  | ClAnd of cl*cl
	  | CommentClAnd of string*cl*cl
	  | Leadsto of pre*cl
	  | Forall of string*cl;;

let freevar_from_term ?(bound = SSet.empty) term =
  match term with
    | Var(x) ->
	if (SSet.mem x bound) then
	  SSet.empty
	else
	  SSet.add x SSet.empty
    | _ -> SSet.empty;;

let freevars_in_termlist ?(bound = SSet.empty) termlist =
  List.fold_left (fun varset term ->
		    let freevar = (freevar_from_term ~bound:bound term) in
		      SSet.union freevar varset
		 ) SSet.empty termlist;;

let rec freevars_in_pre ?(bound = SSet.empty) pre =
  match pre with
    | (PPredicate(_, termlist) | NegPredicate(_, termlist)) ->
	freevars_in_termlist ~bound:bound termlist
    | (PreAnd(pre1, pre2) | Or(pre1, pre2)) ->
	SSet.union (freevars_in_pre ~bound:bound pre1) (freevars_in_pre ~bound:bound pre2)
    | Exists(x, pre) ->
	freevars_in_pre ~bound:(SSet.add x bound) pre
    | (Equal(term1, term2) | NEqual(term1, term2)) ->
	SSet.union
	  (freevar_from_term ~bound:bound term1)
	  (freevar_from_term ~bound:bound term2);;

let rec string_of_term term =
  match term with
    | Const(c) -> "\"" ^ c ^ "\""
    | Var(x) -> "\"" ^ x ^ "\""
    | FuncApp(func, termlist) ->
	string_of_predicate func termlist

and string_of_predicate rel termlist =
  let (term, trest) = ((List.hd termlist), (List.tl termlist)) in
    rel ^ "(" ^ (string_of_term term) ^
      (List.fold_left (
	 fun termstring term ->
	   termstring ^ ", " ^ (string_of_term term)) "" trest)
    ^ ")";;

let rec string_of_pre pred =
  match pred with
    | PPredicate(rel, termlist) ->
	string_of_predicate rel termlist
    | NegPredicate(rel, termlist) ->
	"!" ^ (string_of_predicate rel termlist)
    | PreAnd(pre1, pre2) ->
	Printf.sprintf "%s & %s" (string_of_pre pre1) (string_of_pre pre2)
    | Or(pre1, pre2) ->
	Printf.sprintf "(%s | %s)" (string_of_pre pre1) (string_of_pre pre2)
    | Exists(str, pre) ->
	Printf.sprintf "(E %s.%s)" str (string_of_pre pre)
    | Equal(term1, term2) ->
	Printf.sprintf "%s = %s" (string_of_term term1) (string_of_term term2)
    | NEqual(term1, term2) ->
	Printf.sprintf "%s != %s" (string_of_term term1) (string_of_term term2);;

let rec string_of_cl ?(commented = false) clause =
  match clause with
    | CPredicate(rel, termlist) ->
	string_of_predicate rel termlist
    | Truth -> "1"
    | ClAnd(cl1, cl2) ->
	Printf.sprintf "%s & %s" (string_of_cl ~commented:commented cl1) (string_of_cl ~commented:commented cl2)
    | CommentClAnd(com, cl1, cl2) ->
	if commented = false then
	  Printf.sprintf "%s & %s" (string_of_cl cl1) (string_of_cl cl2)
	else
	  Printf.sprintf "\n\n\n#%s\n\n%s & %s" com (string_of_cl ~commented:commented cl1) (string_of_cl ~commented:commented cl2)
    | Leadsto(pre, cl) ->
	Printf.sprintf "((%s) => %s)" (string_of_pre pre) (string_of_cl ~commented:commented cl)
    | Forall(str, cl) ->
	Printf.sprintf "(A %s.%s)" str (string_of_cl ~commented:commented cl);;


let rec latex_of_term term =
  match term with
    | Const(c) -> "\\Const{" ^ c ^ "}"
    | Var(x) -> "\\Var{" ^ x ^ "}"
    | FuncApp(func, termlist) ->
	latex_of_predicate func termlist

and latex_of_predicate rel termlist =
  let (term, trest) = ((List.hd termlist), (List.tl termlist)) in
    "\\Rel{" ^ rel ^ "} (" ^ (latex_of_term term) ^
      (List.fold_left (
	 fun termstring term ->
	   termstring ^ ", " ^ (latex_of_term term)) "" trest)
    ^ ")";;

let rec latex_of_pre pred =
  match pred with
    | PPredicate(rel, termlist) ->
	latex_of_predicate rel termlist
    | NegPredicate(rel, termlist) ->
	"\\neg" ^ (latex_of_predicate rel termlist)
    | PreAnd(pre1, pre2) ->
	Printf.sprintf "%s \\land %s" (latex_of_pre pre1) (latex_of_pre pre2)
    | Or(pre1, pre2) ->
	Printf.sprintf "(%s \\lor %s)" (latex_of_pre pre1) (latex_of_pre pre2)
    | Exists(str, pre) ->
	Printf.sprintf "\\exists \\Const{%s}.%s" str (latex_of_pre pre)
    | Equal(term1, term2) ->
	Printf.sprintf "%s = %s" (latex_of_term term1) (latex_of_term term2)
    | NEqual(term1, term2) ->
	Printf.sprintf "%s \\not= %s" (latex_of_term term1) (latex_of_term term2);;

let rec latex_of_cl clause =
  match clause with
    | CPredicate(rel, termlist) ->
	latex_of_predicate rel termlist
    | Truth -> "\\Const{1}"
    | ClAnd(cl1, cl2) ->
	Printf.sprintf "%s \\land %s" (latex_of_cl cl1) (latex_of_cl cl2)
    | CommentClAnd(com, cl1, cl2) ->
	Printf.sprintf "\n\n%s\n\n%s & %s" com (latex_of_cl cl1) (latex_of_cl cl2)
    | Leadsto(pre, cl) ->
	Printf.sprintf "(%s) \\Ra %s" (latex_of_pre pre) (latex_of_cl cl)
    | Forall(str, cl) ->
	Printf.sprintf "\\forall \\Const{%s}.%s" str (latex_of_cl cl);;
